home *** CD-ROM | disk | FTP | other *** search
/ Language/OS - Multiplatform Resource Library / LANGUAGE OS.iso / prolog / prlgbnch.lha / prover.pl < prev    next >
Text File  |  1990-05-25  |  2KB  |  99 lines
  1. % generated: 30 October 1989
  2. % option(s): 
  3. %
  4. %   prover
  5. %
  6. %   Richard A. O'Keefe
  7. %
  8. %   Prolog theorem prover
  9. %
  10. %   from "Prolog Compared with Lisp?," SIGPLAN Notices, v. 18 #5, May 1983
  11.  
  12. :-include('Modal_entry').
  13.  
  14. % op/3 directives
  15.  
  16. :- op(950, xfy, #).    % disjunction
  17. :- op(850, xfy, &).    % conjunction
  18. :- op(500, fx, +).    % assertion
  19. :- op(500, fx, -).    % denial
  20.  
  21. prover :- problem(_, P, C),
  22.       implies(P, C),
  23.       fail.
  24. prover.
  25.  
  26. % problem set
  27.  
  28. problem( 1, -a, +a).
  29.  
  30. problem( 2, +a, -a & -a).
  31.  
  32. problem( 3, -a, +to_be # -to_be).
  33.  
  34. problem( 4, -a & -a, -a).
  35.  
  36. problem( 5, -a, +b # -a).
  37.  
  38. problem( 6, -a & -b, -b & -a).
  39.  
  40. problem( 7, -a, -b # (+b & -a)).
  41.  
  42. problem( 8, -a # (-b # +c), -b # (-a # +c)).
  43.  
  44. problem( 9, -a # +b, (+b & -c) # (-a # +c)).
  45.  
  46. problem( 10, (-a # +c) & (-b # +c), (-a & -b) # +c).
  47.  
  48. % Prolog theorem prover
  49.  
  50. implies(Premise, Conclusion) :-
  51.     opposite(Conclusion, Denial),
  52.     add_conjunction(Premise, Denial, fs([],[],[],[])).
  53.  
  54. opposite(F0 & G0, F1 # G1) :- !,
  55.     opposite(F0, F1),
  56.     opposite(G0, G1).
  57. opposite(F1 # G1, F0 & G0) :- !,
  58.     opposite(F1, F0),
  59.     opposite(G1, G0).
  60. opposite(+Atom, -Atom) :- !.
  61. opposite(-Atom, +Atom).
  62.  
  63. add_conjunction(F, G, Set) :-
  64.     expand(F, Set, Mid),
  65.     expand(G, Mid, New),
  66.     refute(New).
  67.  
  68. expand(_, refuted, refuted) :- !.
  69. expand(F & G, fs(D,_,_,_), refuted) :-
  70.     includes(D, F & G), !.
  71. expand(F & G, fs(D,C,P,N), fs(D,C,P,N)) :-
  72.     includes(C, F & G), !.
  73. expand(F & G, fs(D,C,P,N), New) :- !,
  74.     expand(F, fs(D,[F & G|C],P,N), Mid),
  75.     expand(G, Mid, New).
  76. expand(F # G, fs(D,C,P,N), Set) :- !,
  77.     opposite(F # G, Conj),
  78.     extend(Conj, D, C, D1, fs(D1,C,P,N), Set).
  79. expand(+Atom, fs(D,C,P,N), Set) :- !,
  80.     extend(Atom, P, N, P1, fs(D,C,P1,N), Set).
  81. expand(-Atom, fs(D,C,P,N), Set) :-
  82.     extend(Atom, N, P, N1, fs(D,C,P,N1), Set).
  83.  
  84. includes([Head|_], Head) :- !.
  85. includes([_|Tail], This) :- includes(Tail, This).
  86.  
  87. extend(Exp, _, Neg, _, _, refuted) :- includes(Neg, Exp), !.
  88. extend(Exp, Pos, _, Pos, Set, Set) :- includes(Pos, Exp), !.
  89. extend(Exp, Pos, _, [Exp|Pos], Set, Set).
  90.  
  91. refute(refuted) :- !.
  92. refute(fs([F1 & G1|D], C, P, N)) :-
  93.     opposite(F1, F0),
  94.     opposite(G1, G0),
  95.     Set = fs(D, C, P, N),
  96.     add_conjunction(F0, G1, Set),
  97.     add_conjunction(F0, G0, Set),
  98.     add_conjunction(F1, G0, Set).
  99.